#ifndef SAT_SEQ_SOLVER_H
#define SAT_SEQ_SOLVER_H

#include "Problem.h"
//#include "hsl/solver.h"
#include "boost/optional.hpp"
#include <list>
#include <map>
#include <memory>
#include <boost/graph/graph_concepts.hpp>

class LruVariableContainer {
public:
    /* construction */
    
    explicit LruVariableContainer(int numVariables); 
    
    /// insert a variable to be tracked
    void initVariable(Variable v);     

    /* accessor functions */
 
    bool isEmpty() const;
    /// get the variable used least recently 
    Variable getLruVariable() const;
    /// mark v as used recently
    void updateVariableUsed(int iteration, Variable v); 
private:
    typedef int LastChangeIterCount;
    typedef std::pair<LastChangeIterCount, Variable> LruStruct;
    typedef std::list<LruStruct> LruQ_;
    LruQ_ lruQ_;
    typedef std::map<Variable, LruQ_::iterator> VarToQMap;
    VarToQMap varToQMap;
};

class UnsatisfiedClauseContainer {
    typedef std::set<Clause*> Container_;
public:

    /// @return whether there are no unsatisfied clauses
    bool empty() const;
    
    /// delete all recorded clauses
    void clear(); 

    /// use a new solution
    void initializeUnsatisfiedClauses(const Solution& solution);    

    /// update unsatisfied clauses after a variable is changed
    void updateUnsatisfiedClauses(Variable changed);

    /* traverse over unsatisfied clauses */

    typedef Container_::const_iterator ConstIterator;
    ConstIterator begin() const;
    ConstIterator end() const;

    int size() const;

private:
    Container_ unsatisfied_;
    const Solution* solution_;
};

class SATSeqSolver {
public:
    SATSeqSolver(int maxIterCount = 10000); 
    void initializeProblem(const Problem& problem); 
    void solve(); 
    bool done() const;
    bool succeeded() const;
private:
    int getCurrentSolutionCost() const; 
    void flipVariable(Variable v);
    struct VariableGoodness {
        Variable v;
        int goodnessValue; // lower is better
    };
    std::vector<VariableGoodness> findImprovingIntensifyingMoves() const;
    Variable selectVariableToFlip(std::vector<VariableGoodness>& options) const;
    
    bool intensifyMove(); //< returns false if no move could be found
    void diversifyMove();

    const Problem* problem_;
    std::unique_ptr<LruVariableContainer> lru_;
    UnsatisfiedClauseContainer unsatisfied_;
    typedef std::unique_ptr<Solution> SolutionUPtr;
    SolutionUPtr currSol_; //< current solution
    SolutionUPtr bestSol_; //< best solution till now
    int bestSolCost_; //< the cost of the best solution
    int iterCount_;
    int maxIterCount_;
};

#endif
